$\forall$${\it es}$:event\_system\{i:l\}, $e$,${\it e'}$,$a$,$b$:es{-}E(${\it es}$).
\\[0ex]l\_before($a$; $b$; [$e$, ${\it e'}$]; es{-}E(${\it es}$))
\\[0ex]$\Leftarrow\!\Rightarrow$ (es{-}locl(${\it es}$; $a$; $b$) $\wedge$ es{-}le(${\it es}$; $e$; $a$) $\wedge$ es{-}le(${\it es}$; $b$; ${\it e'}$))